ecl-act(ds;da;m;x)
== ecl_ind(x;k,test.L.False;a,b,aa,ab.L.aa(L)
==  (L1, L2:event-info(ds;da) List.
==  (L = (L1 @ L2) & ecl-halt(ds;da;a)(0,L1) & ab(L2));a,b,aa,ab.L.aa(L)
== & (L':event-info(ds;da) List, n:. L'  L  ecl-halt(ds;da;b)(n,L')  L' = L)
==  ab(L)
==  & (L':event-info(ds;da) List, n:. L'  L  ecl-halt(ds;da;a)(n,L')  L' = L);a,b,aa,ab.L.
== aa(L) & (L':event-info(ds;da) List, n:. L'  L  ecl-halt(ds;da;b)(n,L')  L' = L)
==  ab(L)
==  & (L':event-info(ds;da) List, n:.
==  & (L'  L
==  & ( ecl-halt(ds;da;a)(n,L')
==  & ( L'
==  & ( =
==  & ( L);a,aa.star-append(event-info(ds;da);ecl-halt(ds;da;a)
==  & ( L);a,aa.star-append(event-info(ds;da);(0);aa);a,n,aa.if m=n ecl-halt(ds;da;a)(0)
==  & ( L);a,aa.star-append(event-info(ds;da);(0);aa);a,n,aa.else aa fi;a,n,aa.aa;a,l,aa.aa) 

latex

---

clarification:

ecl-act(ds;da;m;x)
== ecl_ind(x;k,test.L.False;a,b,aa,ab.L.aa(L)
==  (L1:event-info(ds;da) List, L2:event-info(ds;da) List.
==  (L = (L1 @ L2)  event-info(ds;da) List & ecl-halt(ds;da;a)(0,L1) & ab(L2));a,b,aa,ab.L.aa(L)
== & (L':event-info(ds;da) List, n:.
== & (L'  L  event-info(ds;da) List  ecl-halt(ds;da;b)(n,L')  L' = L  event-info(ds;da) List)
==  ab(L)
==  & (L':event-info(ds;da) List, n:.
==  & (L'  L  event-info(ds;da) List
==  & ( ecl-halt(ds;da;a)(n,L')
==  & ( L' = L  event-info(ds;da) List);a,b,aa,ab.L.aa(L)
== & (L':event-info(ds;da) List, n:.
== & (L'  L  event-info(ds;da) List  ecl-halt(ds;da;b)(n,L')  L' = L  event-info(ds;da) List)
==  ab(L)
==  & (L':event-info(ds;da) List, n:.
==  & (L'  L  event-info(ds;da) List
==  & ( ecl-halt(ds;da;a)(n,L')
==  & ( L'
==  & ( =
==  & ( L
==  & (  event-info(ds;da) List);a,aa.star-append(event-info(ds;da);ecl-halt(ds;da;a)
==  & (  event-info(ds;da) List);a,aa.star-append(event-info(ds;da);(0);aa);a,n,aa.if m=n
==  & (  event-info(ds;da) List);a,aa.star-append(event-info(ds;da);(0);aa);a,n,aa.if ecl-halt(ds;da;a)
==  & (  event-info(ds;da) List);a,aa.star-append(event-info(ds;da);(0);aa);a,n,aa.if (0)
==  & (  event-info(ds;da) List);a,aa.star-append(event-info(ds;da);(0);aa);a,n,aa.else aa fi;a,n,aa.aa;a,l,aa.aa) 

latex

Definitions	ecl ind, False, x:A. B(x), as @ bs, , x.A(x), P  Q, P & Q, x:A. B(x), , l1  l2, P  Q, s = t, type List, star-append(T;P;Q), event-info(ds;da), if b t else f fi, i=j, f(a), ecl-halt(ds;da;x), #$n
FDL editor aliases	ecl-act